Nuprl Lemma : comb_for_l_succ_wf
4,23
postcript
pdf
(
T
,
l
,
x
,
P
,
z
.
y
= succ(
x
) in
l
P
(
y
))
T
:Type
(
T
List)
T
(
T
Prop)
True
Prop
latex
Definitions
Prop
,
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
l
succ
wf
,
squash
wf
,
true
wf
origin
T,l,x,P,z. y = succ(x) in l
P(y)) 
T:Type
(T List)T(TProp)
TrueProp T,l,x,P,z. y = succ(x) in l P(y)) T:Type(T List)T(TProp)TrueProp T
x:A. B(x)T